Nuprl Lemma : ma-empty-compat-left
0,22
postcript
pdf
A
:MsgA. ||+
A
latex
Definitions
A
||+
B
,
P
&
Q
,
M1
||
M2
,
ma-frame-compatible(
A
;
B
)
,
MsgA
,
x
:
A
.
B
(
x
)
,
t
T
Lemmas
ma-empty-compatible-left
,
ma-empty-frame-compatible-left
,
msga
wf
origin
A:MsgA. ||+ A A:MsgA. ||+ A x:A. B(x)
T